Runtime Complexity (innermost) proof of /tmp/tmpQXkHBQ/Ex4_7_77_Bor03

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS

    ↳1 CpxTrsMatchBoundsTAProof (⇔, 110 ms)

    ↳2 BOUNDS(1, n^1)

    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

        ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳6 CdtProblem

        ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳8 CdtProblem

        ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳10 CdtProblem

        ↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳12 CdtProblem

        ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳14 CdtProblem

        ↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳16 CdtProblem

        ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳18 CdtProblem

        ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳20 CdtProblem

        ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 7 ms)

        ↳22 CdtProblem

        ↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳24 CdtProblem

        ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳26 CdtProblem

        ↳27 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳28 CdtProblem

        ↳29 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳30 CdtProblem

        ↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳32 CdtProblem

        ↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳34 CdtProblem

        ↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳36 CdtProblem

        ↳37 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳38 CdtProblem

        ↳39 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 2 ms)

        ↳40 CdtProblem

        ↳41 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

        ↳42 CdtProblem

        ↳43 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 2 ms)

        ↳44 CdtProblem

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__tail(cons(X, XS)) → mark(XS)
mark(zeros) → a__zeros
mark(tail(X)) → a__tail(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
a__zeros → zeros
a__tail(X) → tail(X)

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 4.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
cons0(0, 0) → 0
00() → 0
zeros0() → 0
tail0(0) → 0
a__zeros0() → 1
a__tail0(0) → 2
mark0(0) → 3
01() → 4
zeros1() → 5
cons1(4, 5) → 1
mark1(0) → 2
a__zeros1() → 3
mark1(0) → 6
a__tail1(6) → 3
mark1(0) → 7
cons1(7, 0) → 3
01() → 3
zeros1() → 1
tail1(0) → 2
02() → 8
zeros2() → 9
cons2(8, 9) → 3
a__zeros1() → 2
a__zeros1() → 6
a__zeros1() → 7
a__tail1(6) → 2
a__tail1(6) → 6
a__tail1(6) → 7
cons1(7, 0) → 2
cons1(7, 0) → 6
cons1(7, 0) → 7
01() → 2
01() → 6
01() → 7
zeros2() → 3
tail2(6) → 3
cons2(8, 9) → 2
cons2(8, 9) → 6
cons2(8, 9) → 7
mark2(0) → 2
mark2(0) → 3
mark2(0) → 6
mark2(0) → 7
zeros2() → 2
zeros2() → 6
zeros2() → 7
tail2(6) → 2
tail2(6) → 6
tail2(6) → 7
mark2(9) → 2
mark2(9) → 3
mark2(9) → 6
mark2(9) → 7
a__zeros3() → 2
a__zeros3() → 3
a__zeros3() → 6
a__zeros3() → 7
04() → 10
zeros4() → 11
cons4(10, 11) → 2
cons4(10, 11) → 3
cons4(10, 11) → 6
cons4(10, 11) → 7
zeros4() → 2
zeros4() → 3
zeros4() → 6
zeros4() → 7
mark2(11) → 2
mark2(11) → 3
mark2(11) → 6
mark2(11) → 7

(2) BOUNDS(1, n^1)

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__ZEROS → c
A__ZEROS → c1
A__TAIL(cons(z0, z1)) → c2(MARK(z1))
A__TAIL(z0) → c3
MARK(zeros) → c4(A__ZEROS)
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(0) → c7

S tuples:

A__ZEROS → c
A__ZEROS → c1
A__TAIL(cons(z0, z1)) → c2(MARK(z1))
A__TAIL(z0) → c3
MARK(zeros) → c4(A__ZEROS)
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(0) → c7

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__ZEROS, A__TAIL, MARK

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing nodes:

A__TAIL(z0) → c3
MARK(0) → c7
A__ZEROS → c1
A__ZEROS → c
MARK(zeros) → c4(A__ZEROS)

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c6(MARK(z0))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c5, c6

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(z0)) → c5(A__TAIL(mark(z0)), MARK(z0)) by

MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(0)) → c5(A__TAIL(0), MARK(0))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(tail(0)) → c5(A__TAIL(0), MARK(0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros), MARK(zeros))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5

(11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0)))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(tail(z0))) → c5(A__TAIL(a__tail(mark(z0))), MARK(tail(z0))) by

MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))
MARK(tail(tail(x0))) → c5(A__TAIL(tail(mark(x0))), MARK(tail(x0)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)), MARK(tail(0)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(15) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(zeros)) → c5(A__TAIL(a__zeros))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(zeros)) → c5(A__TAIL(a__zeros)) by

MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
MARK(tail(zeros)) → c5(A__TAIL(zeros))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
MARK(tail(zeros)) → c5(A__TAIL(zeros))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
MARK(tail(zeros)) → c5(A__TAIL(zeros))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(tail(zeros)) → c5(A__TAIL(zeros))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(tail(tail(0))) → c5(A__TAIL(a__tail(0))) by

MARK(tail(tail(0))) → c5(A__TAIL(tail(0)))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
MARK(tail(tail(0))) → c5(A__TAIL(tail(0)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
MARK(tail(tail(0))) → c5(A__TAIL(tail(0)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(tail(tail(0))) → c5(A__TAIL(tail(0)))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))

S tuples:

A__TAIL(cons(z0, z1)) → c2(MARK(z1))
MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

A__TAIL, MARK

Compound Symbols:

c2, c6, c5, c5

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, z1)) → c2(MARK(z1)) by

A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))

S tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c6, c5, c5, c2

(27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

A__TAIL(cons(z0, tail(zeros))) → c2(MARK(tail(zeros)))
MARK(tail(zeros)) → c5(A__TAIL(cons(0, zeros)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))

S tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)), MARK(tail(zeros)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c6, c5, c5, c2

(29) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))

S tuples:

MARK(cons(z0, z1)) → c6(MARK(z0))
MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c6, c5, c5, c2

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(cons(z0, z1)) → c6(MARK(z0)) by

MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
MARK(tail(tail(x0))) → c5(MARK(tail(x0)))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c5, c2, c6

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(tail(tail(x0))) → c5(MARK(tail(x0))) by

MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1)))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6

(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, cons(y0, y1))) → c2(MARK(cons(y0, y1))) by

A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6

(37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A__TAIL(cons(z0, tail(tail(y0)))) → c2(MARK(tail(tail(y0)))) by

A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(cons(cons(y0, y1), z1)) → c6(MARK(cons(y0, y1))) by

MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6

(41) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(cons(tail(tail(y0)), z1)) → c6(MARK(tail(tail(y0)))) by

MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(cons(tail(tail(tail(tail(y0)))), z1)) → c6(MARK(tail(tail(tail(tail(y0))))))
MARK(cons(tail(tail(tail(cons(y0, y1)))), z1)) → c6(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(tail(tail(tail(zeros))), z1)) → c6(MARK(tail(tail(tail(zeros)))))

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(tail(tail(tail(tail(y0)))), z1)) → c6(MARK(tail(tail(tail(tail(y0))))))
MARK(cons(tail(tail(tail(cons(y0, y1)))), z1)) → c6(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(tail(tail(tail(zeros))), z1)) → c6(MARK(tail(tail(tail(zeros)))))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(tail(tail(tail(tail(y0)))), z1)) → c6(MARK(tail(tail(tail(tail(y0))))))
MARK(cons(tail(tail(tail(cons(y0, y1)))), z1)) → c6(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(tail(tail(tail(zeros))), z1)) → c6(MARK(tail(tail(tail(zeros)))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6

(43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MARK(tail(tail(tail(y0)))) → c5(MARK(tail(tail(y0)))) by

MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
MARK(tail(tail(tail(tail(tail(y0)))))) → c5(MARK(tail(tail(tail(tail(y0))))))
MARK(tail(tail(tail(tail(cons(y0, y1)))))) → c5(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(tail(tail(tail(tail(zeros))))) → c5(MARK(tail(tail(tail(zeros)))))

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

a__zeros → cons(0, zeros)
a__zeros → zeros
a__tail(cons(z0, z1)) → mark(z1)
a__tail(z0) → tail(z0)
mark(zeros) → a__zeros
mark(tail(z0)) → a__tail(mark(z0))
mark(cons(z0, z1)) → cons(mark(z0), z1)
mark(0) → 0

Tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(tail(tail(tail(tail(y0)))), z1)) → c6(MARK(tail(tail(tail(tail(y0))))))
MARK(cons(tail(tail(tail(cons(y0, y1)))), z1)) → c6(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(tail(tail(tail(zeros))), z1)) → c6(MARK(tail(tail(tail(zeros)))))
MARK(tail(tail(tail(tail(tail(y0)))))) → c5(MARK(tail(tail(tail(tail(y0))))))
MARK(tail(tail(tail(tail(cons(y0, y1)))))) → c5(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(tail(tail(tail(tail(zeros))))) → c5(MARK(tail(tail(tail(zeros)))))

S tuples:

MARK(tail(cons(z0, z1))) → c5(A__TAIL(cons(mark(z0), z1)), MARK(cons(z0, z1)))
MARK(tail(tail(tail(z0)))) → c5(A__TAIL(a__tail(a__tail(mark(z0)))), MARK(tail(tail(z0))))
MARK(tail(tail(cons(z0, z1)))) → c5(A__TAIL(a__tail(cons(mark(z0), z1))), MARK(tail(cons(z0, z1))))
A__TAIL(cons(z0, tail(cons(y0, y1)))) → c2(MARK(tail(cons(y0, y1))))
A__TAIL(cons(z0, tail(tail(zeros)))) → c2(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, tail(tail(tail(y0))))) → c2(MARK(tail(tail(tail(y0)))))
A__TAIL(cons(z0, tail(tail(cons(y0, y1))))) → c2(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(zeros))) → c5(A__TAIL(a__tail(a__zeros)))
MARK(cons(tail(cons(y0, y1)), z1)) → c6(MARK(tail(cons(y0, y1))))
MARK(cons(tail(tail(tail(y0))), z1)) → c6(MARK(tail(tail(tail(y0)))))
MARK(cons(tail(tail(cons(y0, y1))), z1)) → c6(MARK(tail(tail(cons(y0, y1)))))
MARK(cons(tail(tail(zeros)), z1)) → c6(MARK(tail(tail(zeros))))
MARK(tail(tail(cons(y0, y1)))) → c5(MARK(tail(cons(y0, y1))))
MARK(tail(tail(tail(tail(y0))))) → c5(MARK(tail(tail(tail(y0)))))
MARK(tail(tail(tail(cons(y0, y1))))) → c5(MARK(tail(tail(cons(y0, y1)))))
MARK(tail(tail(tail(zeros)))) → c5(MARK(tail(tail(zeros))))
A__TAIL(cons(z0, cons(cons(y0, y1), z2))) → c2(MARK(cons(cons(y0, y1), z2)))
A__TAIL(cons(z0, cons(tail(cons(y0, y1)), z2))) → c2(MARK(cons(tail(cons(y0, y1)), z2)))
A__TAIL(cons(z0, cons(tail(tail(tail(y0))), z2))) → c2(MARK(cons(tail(tail(tail(y0))), z2)))
A__TAIL(cons(z0, cons(tail(tail(cons(y0, y1))), z2))) → c2(MARK(cons(tail(tail(cons(y0, y1))), z2)))
A__TAIL(cons(z0, cons(tail(tail(y0)), z2))) → c2(MARK(cons(tail(tail(y0)), z2)))
A__TAIL(cons(z0, cons(tail(tail(zeros)), z2))) → c2(MARK(cons(tail(tail(zeros)), z2)))
A__TAIL(cons(z0, tail(tail(tail(tail(y0)))))) → c2(MARK(tail(tail(tail(tail(y0))))))
A__TAIL(cons(z0, tail(tail(tail(cons(y0, y1)))))) → c2(MARK(tail(tail(tail(cons(y0, y1))))))
A__TAIL(cons(z0, tail(tail(tail(zeros))))) → c2(MARK(tail(tail(tail(zeros)))))
MARK(cons(cons(cons(y0, y1), z1), z2)) → c6(MARK(cons(cons(y0, y1), z1)))
MARK(cons(cons(tail(cons(y0, y1)), z1), z2)) → c6(MARK(cons(tail(cons(y0, y1)), z1)))
MARK(cons(cons(tail(tail(tail(y0))), z1), z2)) → c6(MARK(cons(tail(tail(tail(y0))), z1)))
MARK(cons(cons(tail(tail(cons(y0, y1))), z1), z2)) → c6(MARK(cons(tail(tail(cons(y0, y1))), z1)))
MARK(cons(cons(tail(tail(y0)), z1), z2)) → c6(MARK(cons(tail(tail(y0)), z1)))
MARK(cons(cons(tail(tail(zeros)), z1), z2)) → c6(MARK(cons(tail(tail(zeros)), z1)))
MARK(cons(tail(tail(tail(tail(y0)))), z1)) → c6(MARK(tail(tail(tail(tail(y0))))))
MARK(cons(tail(tail(tail(cons(y0, y1)))), z1)) → c6(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(cons(tail(tail(tail(zeros))), z1)) → c6(MARK(tail(tail(tail(zeros)))))
MARK(tail(tail(tail(tail(tail(y0)))))) → c5(MARK(tail(tail(tail(tail(y0))))))
MARK(tail(tail(tail(tail(cons(y0, y1)))))) → c5(MARK(tail(tail(tail(cons(y0, y1))))))
MARK(tail(tail(tail(tail(zeros))))) → c5(MARK(tail(tail(tail(zeros)))))

K tuples:none
Defined Rule Symbols:

a__zeros, a__tail, mark

Defined Pair Symbols:

MARK, A__TAIL

Compound Symbols:

c5, c2, c5, c6